#ifndef __SOLVER_FUNCTION_H__
#define __SOLVER_FUNCTION_H__

#include "solver_constant.h"

// Inter-block mutex is not reliable.
/*
__device__ __forceinline__
void lock_mutex( void )
{ while( atomicCAS( &__dev_globalMutex, 0, 1 ) != 0 ); }

__device__ __forceinline__
void unlock_mutex( void )
{ atomicExch( &__dev_globalMutex, 0 ); }
*/
/*
__device__ __forceinline__
int get_litArr( int i )
{
#ifdef ASSERT
	if ( (i >= __dev_litArrSize) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: litArr[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return -1;
	}
#endif
	return __dev_litArr[i];
}
*/
__device__ __forceinline__
Lit get_unitClaArr( int i )
{
#ifdef ASSERT
	if ( (i >= __dev_unitClaArrSize) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get unitClaArr[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		//return Lit();
	}
#endif
	return __dev_unitClaArr[i];
}

__device__ __forceinline__
Lit get_claArr( int i )
{
#ifdef ASSERT
	if ( (i >= __dev_claArrSize) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get claArr[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		//return Lit();
	}
#endif
	return __dev_claArr[i];
}

__device__ __forceinline__
Lit* get_claArrPointer( int i )
{
#ifdef ASSERT
	if ( (i >= __dev_claArrSize) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get claArr[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return NULL;
	}
#endif
	return &__dev_claArr[i];
}
/*
__device__ __forceinline__
int get_litArrIndex( int i )
{
#ifdef ASSERT
	if ( (i >= __dev_litArrIndexSize) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: varArrIndex[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return -1;
	}
#endif
	return __dev_litArrIndex[i];
}
*/
__device__ __forceinline__
int get_claArrIndex( int i )
{
#ifdef ASSERT
	if ( (i >= __dev_claArrIndexSize) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get claArrIndex[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return -1;
	}
#endif
	return __dev_claArrIndex[i];
}

__device__ __forceinline__
Lbool get_varAssignment( Lbool* a, int i )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get varAssignment[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return Lbool();
	}
#endif
	return a[i];
}

__device__ __forceinline__
void set_varAssignment( Lbool* a, int i, Lbool v )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set varAssignment[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	a[i] = v;
}

__device__ __forceinline__
int get_varOrder( int* a, int i )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get varOrder[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return -1;
	}
#endif
	return a[i];
}

__device__ __forceinline__
void set_varOrder( int* a, int i, int v )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set varOrder[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	a[i] = v;
}
/*
__device__ __forceinline__
Vec<Clause*>* get_watchListPointer( Vec<Clause*>** a, int i )
{
#ifdef ASSERT
	if ( (i >= __dev_litNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: watchListPointer[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return NULL;
	}
#endif
	return a[i];
}

__device__ __forceinline__
void set_watchListPointer( Vec<Clause*>** a, int i, Vec<Clause*>* v )
{
#ifdef ASSERT
	if ( (i >= __dev_litNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: watchListPointer[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	a[i] = v;
}
*/
__device__ __forceinline__
Lit* get_watchPointer( Lit** a, int i )
{
#ifdef ASSERT
/*
	//lock_global_mutex();
	if ( i >= ((*__dev_clausePtrIndexSize) << 1) || (i < 0) )
	{
		//unlock_global_mutex();
		printf( "tId #%d bId #%d: Assertion fail: watchPointer[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		//return NULL;
		return a[i];
	}
	//unlock_global_mutex();
*/
	if ( i >= ((*__dev_clausePtrIndexSize) << 1) || (i < 0) )
	{
		if ( a[i] == NULL )
		{ printf("tId #%d, bId #%d: get watchPointer[%d] = NULL\n", threadIdx.x, blockIdx.x, i ); }
	}
#endif
	return a[i];
}

__device__ __forceinline__
void set_watchPointer( Lit** a, int i, Lit* v )
{
#ifdef ASSERT
/*
	//lock_global_mutex();
	if ( i >= ((*__dev_clausePtrIndexSize) << 1) || (i < 0) )
	{
		//unlock_global_mutex();
		printf( "tId #%d bId #%d: Assertion fail: watchPointer[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		//return;
		a[i] = v;
	}
	//unlock_global_mutex();
*/
	if ( i >= ((*__dev_clausePtrIndexSize) << 1) || (i < 0) )
	{
		if ( a[i] != NULL )
		{ printf("tId #%d, bId #%d: set old watchPointer[%d] != NULL\n", threadIdx.x, blockIdx.x, i ); }
	}
#endif
	a[i] = v;
}

__device__ __forceinline__
Lit get_trail( Lit* a, int i )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get trail[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return Lit();
	}
#endif
	return a[i];
}

__device__ __forceinline__
void set_trail( Lit* a, int i, Lit v )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set trail[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	a[i] = v;
}

__device__ __forceinline__
int get_decisionLevel( int* a, int i )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get decisionLevel[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return -1;
	}
#endif
	return a[i];
}

__device__ __forceinline__
void set_decisionLevel( int* a, int i, int v )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set decisionLevel[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	a[i] = v;
}

__device__ __forceinline__
bool get_varSeenMarker( bool* a, int i )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get litSeenMarker[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return false;
	}
#endif
	return a[i];
}

__device__ __forceinline__
void set_varSeenMarker( bool* a, int i, bool v )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set litSeenMarker[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	a[i] = v;
}

__device__ __forceinline__
Clause* get_antecedentPointer( Clause** a, int i )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get antecedentPointer[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return NULL;
	}
#endif
	return a[i];
}

__device__ __forceinline__
void set_antecedentPointer( Clause** a, int i, Clause* v )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set antecedentPointer[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	a[i] = v;
}

__device__ __forceinline__
unsigned int get_conflictCount( int i )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get conflictCount[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return 0;
	}
#endif
	return __dev_conflictCount[i];
}

__device__ __forceinline__
void set_conflictCount( int i, unsigned int v )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set conflictCount[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	__dev_conflictCount[i] = v;
}

__device__ __forceinline__
unsigned int get_decisionCount( int i )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get decisionCount[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return 0;
	}
#endif
	return __dev_decisionCount[i];
}

__device__ __forceinline__
void set_decisionCount( int i, unsigned int v )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set decisionCount[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	__dev_decisionCount[i] = v;
}

__device__ __forceinline__
unsigned int get_propagationCount( int i )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get propagationCount[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return 0;
	}
#endif
	return __dev_propagationCount[i];
}

__device__ __forceinline__
void set_propagationCount( int i, unsigned int v )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set propagationCount[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	__dev_propagationCount[i] = v;
}

__device__ __forceinline__
unsigned int get_conflictLitCount( int i )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get conflictLitCount[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return 0;
	}
#endif
	return __dev_conflictLitCount[i];
}

__device__ __forceinline__
void set_conflictLitCount( int i, unsigned int v )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set conflictLitCount[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	__dev_conflictLitCount[i] = v;
}

__device__ __forceinline__
Lbool get_satResult( int i )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get satResult[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return Lbool();
	}
#endif
	return __dev_satResult[i];
}

__device__ __forceinline__
void set_satResult( int i, Lbool v )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set satResult[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	__dev_satResult[i] = v;
}
/*
__device__ __forceinline__
Lbool get_unitVar( int i )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get unitVar[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return false;
	}
#endif
	return __dev_unitVar[i];
}

__device__ __forceinline__
void set_unitVar( int i, Lbool v )
{
#ifdef ASSERT
	if ( (i >= __dev_varNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set unitVar[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	__dev_unitVar[i] = v;
}
*/

__device__ __forceinline__
Lit get_unitClauseLit( int i )
{
#ifdef ASSERT
	if ( (i >= __dev_unitClauseLitSize) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get unitClauseLit[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return __dev_unitClauseLit[i];
	}
#endif
	return __dev_unitClauseLit[i];
}

__device__ __forceinline__
void set_unitClauseLit( int i, Lit v )
{
#ifdef ASSERT
	if ( (i >= __dev_unitClauseLitSize) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set unitClauseLit[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		__dev_unitClauseLit[i] = v;
	}
#endif
	__dev_unitClauseLit[i] = v;
}

__device__ __forceinline__
Clause* get_clausePtrIndex( int i )
{
#ifdef ASSERT
	if ( (i >= (*__dev_clausePtrIndexSize)) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get clausePtrIndex[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return __dev_clausePtrIndex[i];
	}
#endif
	return __dev_clausePtrIndex[i];
}

__device__ __forceinline__
void set_clausePtrIndex( int i, Clause* v )
{
#ifdef ASSERT
	if ( (i >= (*__dev_clausePtrIndexSize)) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set clausePtrIndex[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		__dev_clausePtrIndex[i] = v;
	}
#endif
	__dev_clausePtrIndex[i] = v;
}

__device__ __forceinline__
float get_clauseActivityKey( int i )
{
#ifdef ASSERT
	if ( (i >= (*__dev_clausePtrIndexSize)) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get clauseActivityKey[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return __dev_clauseActivityKey[i];
	}
#endif
	return __dev_clauseActivityKey[i];
}

__device__ __forceinline__
void set_clauseActivityKey( int i, float v )
{
#ifdef ASSERT
	if ( (i >= (*__dev_clausePtrIndexSize)) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set clauseActivityKey[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		__dev_clauseActivityKey[i] = v;
	}
#endif
	__dev_clauseActivityKey[i] = v;
}

__device__ __forceinline__
Vec<Clause*>* get_watchListPtr( int i )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get watchListPtr[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return NULL;
	}
#endif
	return __dev_watchList[i];
}

__device__ __forceinline__
void set_watchListPtr( int i, Vec<Clause*>* v )
{
#ifdef ASSERT
	if ( (i >= __blocksPerGrid) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: set watchListPtr[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return;
	}
#endif
	__dev_watchList[i] = v;
}

__device__ __forceinline__
Vec<Clause*>* get_watchList( Vec<Clause*>* a, int i )
{
#ifdef ASSERT
	if ( (i >= __dev_litNumber) || (i < 0) )
	{
		printf( "tId #%d bId #%d: Assertion fail: get watchList[%d] out of index range.\n", threadIdx.x, blockIdx.x, i );
		return NULL;
	}
#endif
	return &a[i];
}

#endif /* __SOLVER_FUNCTION_H__ */
